es:ES, e:E, P:({a:E| loc(a) = loc(e)  Id} ).
(a:{a:E| loc(a) = loc(e)  Id} . Dec(P(a)))
 (e'e.P(e')  P(e)  e'e.((P(e')  P(e))) & e''(e',e].P(e'')  P(e)) 

latex

Definitions	A, {T}, A c B, e(e1,e2].P(e), ee'.P(e), ee'.P(e), P  Q, P & Q, P  Q, P  Q, x:A. B(x), Dec(P), t  T, x(s), P  Q, , x:A. B(x), False
Lemmas	es-locl wf, es-le-loc, es-le wf, last-transition, inconsistent-bool-eq2, inconsistent-bool-eq, bool wf, iff wf, bfalse wf, btrue wf, not wf, event system wf, es-E wf, decidable wf, es-loc wf, Id wf